T:(IdType), tab:secret-table(T), kx:((+Atom1)Atom1). decrypt(tab;kx)  data(T)+Unit 

latex

Definitions	t  T, x:A. B(x), data(T), , inr(x), false, Unit, left+right, x:AB(x), , b, A, b, s = t, Prop, inl(x), Type, st-key-match(tab;k1;k2), if b t else f fi, st-lookup(tab;x), Atom$n, , x:AB(x), P  Q, outl(x), A/x,y. B(x;y), isl(x), P & Q, P  Q, decrypt(tab;kval), Id, secret-table(T)
Lemmas	secret-table wf, Id wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, isl wf, outl wf, nat wf, st-lookup wf, ifthenelse wf, st-key-match wf, unit wf, bool wf, bnot wf, not wf, assert wf, bfalse wf, it wf, data wf